#!/bin/tcsh
echo -n "% Problem    : " ; head -2 $1 | tail -1 | sed -e "s/.*  : //"
set ProblemSPC=`grep " SPC " $1 | sed -e "s/.* : //"`
set defaultargs="--delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --free-numbers"
set flags=" --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -tKBO6 -winvfreqrank -c1 -Ginvfreq -F1 -WSelectMaxLComplexAvoidPosPred "
set heuristic=" -H(1.ConjectureTermPrefixWeight(DeferSOS,1,3,0.1,5,0,0.1,1,4),1.ConjectureTermPrefixWeight(DeferSOS,1,3,0.5,100,0,0.2,0.2,4),1.Refinedweight(ConstPrio,4,300,4,4,0.7),1.RelevanceLevelWeight2(PreferProcessed,0,1,2,1,1,1,200,200,2.5,9999.9,9999.9),1.StaggeredWeight(DeferSOS,1),1.SymbolTypeweight(DeferSOS,18,7,-2,5,9999.9,2,1.5),2.Clauseweight(ConstPrio,20,9999,4),2.ConjectureSymbolWeight(DeferSOS,9999,20,50,-1,50,3,3,0.5),2.StaggeredWeight(DeferSOS,2)) "
set final="--cpu-limit="$STAREXEC_CPU_LIMIT" "$1
set ecmd="./eprover ""$defaultargs $flags $heuristic $final"

if ( `expr "$ProblemSPC" : "FOF.*"` || `expr "$ProblemSPC" : "CNF.*"` ) then
	echo "% Command    : " $ecmd
	/home/starexec/bin/GetComputerInfo -p THIS Model CPUModel RAMPerCPU OS | \
        sed -e "s/Computer     /% Computer   /" \
            -e "s/Model        /% Model      /" \
            -e "s/CPUModel     /% CPU        /" \
            -e "s/RAMPerCPU    /% Memory     /" \
            -e "s/OS           /% OS         /"
	echo -n "% CPULimit   : " ; echo "$STAREXEC_CPU_LIMIT"
	echo -n "% DateTime   : " ; date
	echo "% CPUTime    : "
	$ecmd
else
    echo "% SZS status Inappropriate"
endif
